Inference at * 1 
Iof proof for Lemma last-not-before:



1. T : Type
2. L : T List
3. (null(L))
4. no_repeats(T;L)
5. x : T
6. last(L) before x  L
7. x, y:T. x before y  L  ((x = y))
8. (last(L) = x)
  False 

latex

 by ((InstLemma `before_last` [T;L;x]) 
CollapseTHEN (Auto)) 

latex

C1: .....antecedent..... NILNIL

C1:   (x  L)
C2: .....antecedent..... NILNIL

C2:   (x = last(L))
C3: 

C3: 9. x before last(L)  L
C3:   False
C.

Definitions	t  T, (x  l), last(L), b, null(as), P  Q, s = t, x before y  l, no_repeats(T;l), A, type List, Type, Void, x:A. B(x), x:AB(x), False
Lemmas	before last, l member wf